Nuprl Lemma : normalize-constraints_wf
11,40
postcript
pdf
k
:
,
A
:((
:(
)
) List). normalize-constraints(
k
;
A
)
((
:(
)
) List)
latex
Definitions
has-value(
a
)
,
Y
,
P
Q
,
map(
f
;
as
)
,
map-eval(
x
.
f
(
x
);
L
)
,
normalize-constraints(
k
;
A
)
,
t
T
,
x
:
A
.
B
(
x
)
Lemmas
map
wf
,
normalize-constraint
wf
,
rationals
wf
,
nat
wf
origin
k:
, A:((:(
) 
) List). normalize-constraints(k;A) 
((:() ) List) k:, A:((:() ) List). normalize-constraints(k;A) ((:() ) List) 
Q Tx:A. B(x)